%
% Copyright 2017, Data61
% Commonwealth Scientific and Industrial Research Organisation (CSIRO)
% ABN 41 687 119 230.
%
% This software may be distributed and modified according to the terms of
% the BSD 2-Clause license. Note that NO WARRANTY is provided.
% See "LICENSE_BSD2.txt" for details.
%
% @TAG(DATA61_BSD)
%

\documentclass[a4paper,11pt]{article}
\usepackage[colour,nictaonly]{disy}

% Setting this to true turns on the ``draft'' watermark
\newif \ifDraft         \Drafttrue

%%% Hyperlinks embed links for references in the PDF output (both for
%%% internal as well as external links).
\newif \ifhyperlinks    \hyperlinkstrue

%%% When using this you should use \autoref{label} instead of
%%% Section~\ref{label}. This will make ``Section'' part of the link, not
%%% just the number.

% Easy control over page margins. You can use ``right'', ``top'', ...
\usepackage[margin=25mm]{geometry}
%\usepackage[margin=25mm,left=33mm]{geometry}	% better for double-sided reports

\usepackage{graphicx}
\setkeys{Gin}{keepaspectratio=true,clip=true,draft=false,width=\linewidth}
\usepackage{times,cite,url,microtype}
\urlstyle{rm}
\renewcommand{\ttdefault}{cmtt}	% CM rather than courier for \tt

\usepackage{tabularx}

\ifDraft
  \usepackage{draftcopy}
  \newcommand{\Comment}[1]{\textbf{\textsl{#1}}}
  \newcommand{\FIXME}[1]{\textbf{\textsl{FIXME: #1}}}
%  \date{\version}
\else
  \newcommand{\Comment}[1]{\relax}
  \newcommand{\FIXME}[1]{\relax}
  \date{}
\fi

\ifhyperlinks
  \usepackage[pdftex,pagebackref,hyperindex,bookmarks]{hyperref}
  \hypersetup{linktocpage,colorlinks}
\else   
  \providecommand{\href}[2]{\url{#2}}
\fi



\begin{document}

\title{capDL --- Capability Distribution Language Specification}
\author{Gerwin Klein}
\AuthorEmail{gerwin.klein@nicta.com.au}
\maketitle

\noindent
This document defines capDL revision 1.0, a language for capability
distributions.

\section{Background and Purpose}
\label{sec:capDL:purpose}

The purpose of capDL is describing snapshots of a system running on the seL4
microkernel. In particular, it can be used to describe which entities 
have access to which seL4 capabilities.

The main objectives are to use these descriptions for specifying systems, for
security analysis of systems, as input for automated bootstrapping of systems,
and for debugging applications running on seL4. A capDL specification can be
complete, i.e.\ give a full picture of all capabilities in the system, or the
system can be underspecified, showing only the capabilities accessible to a
particular component. It is possible to describe system states in capDL that
are not reachable via actual system executions. It is also possible to leave
out details in a system specification that for instance are not important for
a security analysis (e.g.\ because the relevant authority is already
represented otherwise), but that would be necessary for an actual
implementation of the system.


%\section{Example}
%\label{sec:capDL:example}
%
%Figure \ref{fig:capDL:example} shows a small example specification in capDL.
%
%\FIXME{complete example section}
%
%\begin{figure}
%{\small
%\begin{verbatim}
%arch ia32
%
%objects
%
%io_ports = io_ports 
%
%NIC_A = io_device  -- network A
%TIMER = io_device  -- the TIMER chip 
%
%-- the TIMER component
%
%TIMER_ut = ut {
%  TIMER_tcb = tcb
%  TIMER_cspace = cnode (10 bits)
%  TIMER_frames = frame (4k)
%  TIMER_vspace = pd
%}
%
%NIC_A_frames = frame[4] (4k)  -- IO memory for network card
%
%TIMER_notificationR = notification
%
%caps
%
%TIMER_tcb { 
%  cspace: TIMER_cspace (RW)
%  vspace: TIMER_vspace (RW)
%}
%
%TIMER_cspace {
%  0: TIMER_tcb (RW)
%  1: TIMER_cspace (RW)
%  2: TIMER_notificationC (W)
%  3: TIMER_notificationR (W)
%  4: TIMER (RWG)
%  5: irq_table (irq: 5) -- FIXME
%}
%
%TIMER_vspace {
%  0: TIMER_frames (RW)
%  1: 
%}
%
%NIC_A { 
%  0:   (RW) 
%}
%
%\end{verbatim}}
%  \caption{Example capDL specification.}\label{fig:capDL:example}
%\end{figure}
%

\section{Syntax}
\label{sec:capDL:syntax}

This section gives a complete definition of the capDL syntax in BNF.

\subsection{Lexical Tokens}

The lexical tokens of capDL are numbers (\texttt{number}), identifiers
(\texttt{identifier}), and verbatim symbols and operators typeset between
quotes \texttt{''} in the syntax section below.

Numbers are in decimal, hexadecimal (with prefix 0x), or octal (with prefix 0)
form. Identifiers start with a letter \texttt{[a-zA-Z]}, followed by a
sequence of letters \texttt{[a-zA-Z]}, numbers \texttt{[0-9]}, the
underscore character \texttt{\_}, or a \texttt{@} character.

The language is case sensitive.

Comments can occur between any two tokens and can be nested. A potentially
multiline comment starts with the two characters \texttt{/*} and ends with
\texttt{*/}. A one-line comment starts with \texttt{--}. All characters after
\texttt{--} up to the end of the same line are ignored.

Whitespace (a sequence of space, newline and tab characters) can occur between
any two tokens and is ignored.


\subsection{Syntax}

This section describes the concrete syntax of capDL using the tokens defined above. The main syntactic entity of a file is \texttt{module} defined in \ref{sec:capDL:syntax:module}.

\subsubsection{Names and Ranges}

\begin{verbatim}
  name ::= identifier

  num ::= '[' number ']'
  range ::= number '..' number  | '..' number  | number  '..' | number            
  ranges ::=  '[' ']' | '[' range (',' range)* ']' 

  name_ref ::= name ranges?
  qname ::= name_ref ('/' name_ref)* 
\end{verbatim}

\subsubsection{Object Declarations}

\begin{verbatim}
  obj_decls ::= 'objects' '{' obj_decl* '}'

  obj_decl ::= qname '=' object

  object ::= object_type object_params? opt_obj_decls?

  object_type ::= 'ep'  | 'notification' | 'tcb' | 'cnode' | 'ut' | 'irq' |
                  'asid_pool' | 'pt' | 'pd' | 'frame' | 'io_ports' |
                  'io_device' | 'io_pt' | 'vcpu'

  object_params ::= '(' (object_param (',' object_param)*)? ')'

  object_param   ::= obj_bit_size | obj_vm_size | io_pt_level | obj_ports_size |
                     init_arguments | tcb_dom | obj_paddr | domain_id |
                     pci_device
  obj_bit_size   ::= number 'bits'
  obj_vm_size    ::= number ('k' | 'M')
  io_pt_level    ::= 'level' ':' number
  obj_ports_size ::= number 'k' 'ports'
  init_arguments ::= 'init' ':' '[' (number (',' number)*)? ']'
  tcb_dom        ::= 'dom' ':' number
  obj_paddr      ::= 'paddr' ':' number
  domain_id      ::= 'domainID' ':' number
  pci_device     ::= number ':' number '.' number

  opt_obj_decls ::= '{' ((obj_decl | name_ref) ','?)* '}'
\end{verbatim}


\subsubsection{Capability Declarations}

\begin{verbatim}
  cap_decls ::= 'caps' '{' (cap_name_decl | cap_decl)* '}'

  cap_name_decl ::= name '=' '(' name_ref ',' slot ')'

  slot ::= number | symbolic_slot
  symbolic_slot ::= 'cspace' | 'vspace' | 'reply_slot' | 'caller_slot' |
                    'ipc_buffer_slot'

  cap_decl ::= name_ref '{' (cap_mapping_or_ref ';'?)* '}'

  cap_mapping_or_ref ::= (slot ':')? cap_name? (cap_mapping | cap_name_ref)

  cap_name    ::= name_ref '='
  cap_mapping ::= name_ref cap_params? parent?
  cap_params  ::= '(' cap_param (',' cap_param)* ')' 

  cap_param ::= right+
              | 'masked' ':' right+
              | 'guard' ':' number
              | 'guard_size' ':' number
              | 'badge' ':' number
              | 'ports'  ':' ranges
              | 'reply'
              | 'master_reply'
              | 'asid' ':' asid
              | 'cached'
              | 'uncached'

  right ::= 'R' | 'W' | 'G' | 'X'
  asid ::= '(' number ',' number ')'

  parent ::= '- child_of' slot_ref

  slot_ref ::= '(' name_ref ',' slot ')' | name_ref

  cap_name_ref ::= '<' name_ref '>' cap_params? parent?
\end{verbatim}


\subsubsection{IRQ Declarations}

\begin{verbatim}
  irq_decls ::='irq_maps' '{' (irq_mapping ';'?)* '}'

  irq_mapping ::= (number ':')? name_ref
\end{verbatim}


\subsubsection{CDT Declarations}

\begin{verbatim}
  cdt_decls ::='cdt' '{' cdt_decl* '}'

  cdt_decl ::= slot_ref '{' ((slot_ref | cdt_decl) ';'?)* '}'
\end{verbatim}


\subsubsection{Modules}\label{sec:capDL:syntax:module}

\begin{verbatim}
  arch ::= 'arch' ('ia32' | 'arm11') 

  module ::= arch (obj_decls | cap_decls | irq_decls | cdt_decls)+
\end{verbatim}


\section{Semantics}
\label{sec:capDL:semantics}

In this section we show the semi-formal semantics of capDL in the form of its underlying data model in Haskell and give a brief rationale for its contents. This data model can be made fully formal by mapping it directly into the Isabelle theorem prover via NICTA's existing Haskell-to-Isabelle translation tool. The data model can also be mapped into various output formats. 

After describing the data model below, we outline a semi-formal definition of the semantics: mapping the capDL syntax into the capDL data model.


\subsection{Data Model}

\subsubsection{Rationale}
The purpose of capDL is describing a snapshot of the capability distribution in 
a system running on the seL4 microkernel. For this purpose, we need to know 
which objects exist in the system and which capabilities they have access to. 
The second purpose of capDL is to serve as sufficiently detailed input to 
automated code generation tools. Therefore we need to include all information 
about capability arguments that such implementations will need. Some of this 
information will not be relevant for security analysis. For instance, for a 
security analysis it may be necessary to know which frames of physical memory 
an entity in the system can access via virtual memory, but it is not necessary 
to know under which virtual address each of these physical addresses is visible 
to the process. For a concrete implementation of a bootstrapping component on 
the other hand, this latter information is crucial.

\subsubsection{The Model}
We refer to objects by name. This name could be of any type; for convenience we either use a plain string or a string with an index. We use the \texttt{Maybe} type of Haskell to express this. 

\begin{verbatim}
types ObjID = (String, Maybe Word)
\end{verbatim}

With this the capability state of a system is fully described by a map from \texttt{ObjID} to \texttt{Object}. Since not all objects and capabilities are supported by seL4 on all machine architectures, we also store which architecture the system is intended for.

\begin{verbatim}
data Model =  Model {
                  arch :: Arch,
                  objects :: Map ObjID Object
              } 

data Arch = IA32 | ARM11
\end{verbatim}

Objects are described by the following data type. We are mainly interested in what capabilities an object contains. We also store information that is relevant for creating an object such as its type and its size when the size is configurable. This means in contrast to the security model, where we only talk about abstract entities, we give more detailed information in capDL.

\begin{verbatim}
types CapMap = Map Word Cap

data Object = Endpoint
            | Notification
            | TCB { slots :: CapMap, initArguments :: [Word] }
            | CNode { slots :: CapMap, sizeBits :: Word } 
            | Untyped { maybeSizeBits :: Maybe Word }

            | ASIDPool { slots :: CapMap }
            | PT { slots :: CapMap }
            | PD { slots :: CapMap }
            | Frame { vmSizeBits :: Word }
            | IOPorts { size :: Word }
            | IOPT { slots :: CapMap, level :: Word }
            | IODevice { slots :: CapMap }
\end{verbatim}

The first two objects, communication endpoints and asynchronous endpoints, do not store any capabilities and have a fixed size. Thread Control Blocks (TCB) contain a small number of capability registers, modelled by the field \texttt{slots}, a map from a machine word (the slot/register number) to the capability that is stored in that slot. Slots may be empty. CNode objects are the main capability storage object in seL4. They have configurable size. Untyped objects are conceptual containers for dynamically created objects. They cover a set of objects referred to by their \texttt{ObjID}. This set is called the covering set. In the implementation untyped objects must have a size, but in capDL specifications we often want to leave the size unspecified (as large as necessary). 

The next batch of objects in the data type above are architecture dependent. Most of these data structures and devices do not store actual capabilities in the kernel and hardware implementation. Instead they store pointers or mappings to other resources in the system. Since these resources are already represented as objects, we use capabilities to model these mappings and to express the access, for instance, a device may have to physical memory. In detail, the architecture dependent objects are as follows. ASID pools store which page directories (PD) can be activated by the machine. As mentioned, we represent this mapping as a capability in the model. Analogously, we model the mappings in virtual memory objects page directory (PD) and page table (PT). Physical memory frames (\texttt{Frame}) come in different sizes, depending on architecture, but do not contain further capabilities. IOMMU page tables (\texttt{IOPT}) come in multiple levels and again store mappings to frames or further page tables. Finally, hardware devices are represented by the object type \texttt{IODevice}. Again, we model the access hardware may have to resources in the system as capabilities. Specifically, IODevices may have a capability to a CNode for IRQ delivery, potentially multiple capabilities to physical memory frames for memory mapped device registers, and one capability for the root IOMMU space. 

To conclude the description of the capDL data model, it remains to define the data type of capabilities \texttt{Cap}. Almost all capabilities in seL4 refer to one specific object. Some may refer to a set of objects or implicitly to all objects of a given type. Many of the capabilities store explicit access rights. These are modelled as follows:

\begin{verbatim}
data Rights = Read | Write | Grant
types CapRights = Set Right
\end{verbatim}

Again in contrast to the security model of seL4, we explicitly distinguish different types of capabilities in capDL and store slightly different kinds of additional information with each. As a side effect, we do not need an explicit representation of the create right. The create right is conferred by the possession of an untyped capability.

{\small
\begin{verbatim}
data Cap = NullCap
         | UntypedCap { capObj :: ObjID } 
         | EndpointCap { capObj :: ObjID, capBadge :: Word, capRights :: CapRights }
         | NotificationCap { capObj :: ObjID, capBadge :: Word, capRights :: CapRights }
         | ReplyCap { capObj :: ObjID }
         | MasterReplyCap { capObj :: ObjID }
         | CNodeCap { capObj :: ObjID, capGuard :: Word, 
                      capGuardSize :: Word }
         | TCBCap { capObj :: ObjID }
         | IRQControlCap 
         | IRQHandlerCap { capObj :: ObjID }
         | FrameCap { capObj :: ObjID, capRights :: CapRights } 
         | PTCap { capObj :: ObjID } 
         | PDCap { capObj :: ObjID }
         | ASIDControlCap 
         | ASIDPoolCap { capObj :: ObjID }
         | IOPortsCap { capObjs :: Set Word }
         | IOSpaceMasterCap 
         | IOSpaceCap { capObj :: ObjID }
         | IOPTCap { capObj :: ObjID }
\end{verbatim}}

In detail, the capabilities are as follows. We go through the list of 
capabilities and give a brief indication of the authority they convey. The 
\texttt{NullCap} is occasionally used to represent the absence of a capability. 
An untyped capability points to an untyped object and confers the right to 
issue create/retype and revoke/delete operations. Endpoint and asynchronous 
endpoint capabilities point to their respective object types. They explicitly 
store which Read/Write/Grant access is conferred to the communications channel 
and they may carry one machine word of additional information, called the 
badge. CNode capabilities in addition to their CNode object reference carry 
information that influences the lookup of capabilities in the node they point 
to. This information consists of a guard in the sense of guarded page tables, 
the size of that guard, and finally the rights to the CNode object itself. A 
TCB cap gives authority over one TCB object with given access rights. The 
IRQControl capability gives authority to create specific IRQHandler 
capabilities. Each device may have a special CNode associated with it that may 
contain an asynchronous endpoint which in turn is used to deliver interrupts to 
user level. IRQHandler caps in capDL point to these specific CNodes. It confers 
the authority to change which endpoint the interrupt is delivered to. Frame 
capabilities confer authority to map and unmap physical memory frames into and 
from a page directory or page table with the specified access rights. PT caps 
give authority to map/unmap page tables into/from page directories and PD caps 
give the authority to map/unmap page directories into ASID pools and to install 
them as virtual memory space of a process. The ASIDControlCap together with an 
Untyped cap confers authority to create new ASID pools. Only a limited, fixed 
number can be created in the system. ASIDPool caps give the authority to 
map/unmap page directories into/from the ASID pool. Mapping a frame into a page 
table for instance, needs the frame cap to specify which frame to map with 
which rights and the PT cap to specify in which page table. The IOPorts 
capability gives access to a set of IOPorts on the ia32 architecture. The 
IOSpaceMasterCap confers the authority to create IOSpace caps for specific 
devices. IOSpaceCaps point to IODevices and confer the authority to set the 
root IOPageTable for that device. IOPTCaps are the IOMMU analogue to PT and PD 
caps in normal virtual memory.



\subsection{Semantics}

In this section, we define a mapping from the syntax of capDL to the data model of capDL. The mapping is defined by going over the relevant productions in the capDL grammar and describing the corresponding model.

\subsubsection{Names and Ranges}

\begin{verbatim}
  name ::= identifier
\end{verbatim}

Names are mapped to \texttt{ObjID}s in the model. A name without index maps to \texttt{(name, Nothing)}. Qualified names will be defined in the object declaration section.

\begin{verbatim}
  num ::= '[' number ']'
\end{verbatim}
This production maps to a single index and is used to either declare a set of objects, in which case the number is the number of objects, or to refer to a specific index. The term name[x] maps to the \texttt{ObjID} \texttt{(name, Just x)}.

\begin{verbatim}
  range ::= number '..' number  | '..' number  | number  '..' | number            
  ranges ::=  '[' ']' | '[' range (',' range)* ']' 
  name_ref ::= name ranges?
\end{verbatim}

Ranges stand for sets of \texttt{ObjID}s. For a set declared as name[n], the following mappings apply:

\begin{itemize}
  \item name[..b] refers to name[0], name[1], .., name[b] 
  \item name[a..] refers to name[a], name[a+1], .., name[n]
  \item name[a..b] refers to name[a], name[a+1], .., name[b]
  \item name[] refers to name[0], name[1], .., name[n] 
\end{itemize}

A list of ranges name[r1,r2,..r3] refers to the union of the ranges name[r1], name[r2], .., name[r3].

\subsubsection{Module}

\begin{verbatim}
  arch ::= 'arch' ('ia32' | 'arm11') 
  module ::= arch (obj_decls | cap_decls)+ 
\end{verbatim}

A module maps to a full \texttt{Model} in the data model. Its \texttt{Arch} component is determined by \texttt{arch}, its mapping from \texttt{ObjID} to \texttt{Object} by the object and capability declarations described below.


\subsubsection{Object Declarations}

\begin{verbatim}
  obj_decls ::= 'objects' obj_decl*
\end{verbatim}

An object declaration section defines a set of objects. Each object name of typed objects should be declared only once. The covering set of untyped objects may be declared multiple times. The total covering set is the union of all covering sets mentioned for that object.

\begin{verbatim}
  obj_decl ::= qname '=' object
\end{verbatim}

An object declaration has a potentially qualified name and dimension on the left hand side and an object content declaration on the right hand side. A qualified name \texttt{name1/name2/name3[n]} implicitly declares the untyped objects \texttt{name1} and \texttt{name2}. It also declares that \texttt{name2} is covered by \texttt{name1} and \texttt{name3} covered by \texttt{name2}. Giving a dimension \texttt{[n]} means that n objects \texttt{(name3, Just 0)} to \texttt{(name3, Just (n-1))} are declared, each with the same content described on the right hand side of the equation.

The right hand side is defined by the following syntax productions:

\begin{verbatim}
  object ::= object_type object_params? obj_decls?

  object_type ::= 'ep'  | 'notification' | 'tcb' | 'cnode' | 'ut' | 
                  'asid_pool' | 'pt' | 'pd' | 'frame' | 'io_ports' |
                  'io_device' | 'io_pt' 

  object_params ::= '(' object_param (',' object_param)* ')'

  object_param   ::= obj_bit_size | obj_vm_size | io_pt_level | obj_ports_size
  obj_bit_size   ::= number 'bits'
  obj_vm_size    ::= number ('k' | 'M')
  io_pt_level    ::= 'level' ':' ('1' | '2' | '3')
  obj_ports_size ::= number 'k' 'ports'

  obj_decls ::= '{' ((obj_decl | name_ref) ','?)* '}'
\end{verbatim}

The object content is given by the type of the object mapping to its 
corresponding object type in the data model. Some of the object types in the 
model require a size parameter, given in bits (where n bits means a size of 
$2^n$ entries). Frames' sizes are specified directly as are the levels of IOMMU 
page tables. Untyped objects can be followed by a nested object declaration. 
Writing 

\begin{verbatim}
name1 = ut {
  name2/name3 [n] = object
  name2/name4 = object
 ...
}
\end{verbatim}

is equivalent to writing

\begin{verbatim}
name1/name2/name3 [n] = object
name1/name2/name4 = object
...
\end{verbatim}


\subsubsection{Capability Declarations}

The capability content of objects is declared in its own section, separately from the list of objects itself.

\begin{verbatim}
  cap_decls = 'caps' (cap_name_decl | cap_decl)*

  cap_name_decl ::= name '=' '(' name_ref ',' slot ')'
  slot ::= number | symbolic_slot
  symbolic_slot ::= 'cspace' | 'vspace' 
\end{verbatim}

Next to capability content declarations, there are name declarations for capability slots. A capability slot is defined by the container object, referred to by a name reference (mapping to a single \texttt{ObjID}) and a slot inside the container specified by its slot number. The symbolic slot names cspace, vspace stand for slot numbers 0 and 1.

A capability declaration starts with a set of container objects, each of which is declared to contain the capability mappings specified on the right hand side. Container objects may occur more than once in a specification. Their mappings are the union of all mappings for that container object.

\begin{verbatim}
  cap_decl ::= name_ref '{' (cap_mapping_or_ref ';'?)* '}'
\end{verbatim}

A cap mapping is specified by its slot and its capability and potentially an inline name declaration for the specified slot in the specified container. 

\begin{verbatim}
  cap_mapping_or_ref ::= slot ':' cap_name? (cap_mapping | cap_name_ref)

  cap_name    ::= name '='
  cap_mapping ::= name_ref cap_params?
  cap_params  ::= '(' cap_param (',' cap_param)* ')' 

  cap_param ::= right+
              | 'masked' ':' right+
              | 'guard' ':' number
              | 'guard_size' ':' number
              | 'irq'
              | 'badge' ':' number
              | 'reply'
              | 'master_reply'

  right ::= 'R' | 'W' | 'G'

  cap_name_ref ::= '<' name_ref '>' cap_params?
\end{verbatim}

The capability declaration is either a \texttt{cap\_mapping} or 
\texttt{cap\_name\_ref}. In the latter case the mapping is a copy of the 
capability in the slot referred to by \texttt{name} (possibly \texttt{masked} 
with an access rights mask). In the former case, a cap is defined by the object 
it points to, together with optional parameters depending on the type of the 
object in the data model. For instance, an endpoint cap is specified if the 
\texttt{ObjID} given in the cap declaration refers to an endpoint object. If no 
parameters are mentioned, default parameters are substituted if possible. These 
defaults are: empty set of rights for access rights, full set of rights for 
rights masks, guard 0, guard size 0, and badge 0. The IRQControl cap is 
specified using the reserved \texttt{ObjID} \texttt{irq\_control}, similarly 
ASIDControlCap is specified by \texttt{asid\_control} and IOSpaceMasterCap by 
\texttt{io\_space\_master}.

%FIXME: IO Ports


%\subsection{Mapping into Security Model}
%
%This section shows a mapping from the capDL data model into a formal security model such as the one used in section \ref{sec:security-model}. The mapping presented here is not machine-checked and not complete, its purpose is to sketch how a formal mapping may look like.
%
%The main differences between the security model and the capDL model are in the additional detail that is represented in capDL. To translate a capDL model state into a security model state, we need to translate all capDL objects into security entities, all capDL capabilities into security model capabilities, and all capDL ObjIDs into security model entity-ids.
%
%The security model uses addresses as entity identifiers, the capDL model uses names with potential indicies. Since each capDL model is finite, we can just enumerate all ObjIDs mentioned in this model and use the position of the ObjID in that enumeration as the corresponding security model address. In other words, if there are $n$ objects in the capDL model then there exists a bijective mapping function \texttt{id\_of} from the ObjIDs of this model into the numbers $\{1..n\}$. 
%
%In the security model, the main content of an entity is the set of caps it has access to. We do not record size or other parameters of the object or slot numbers of capability mappings. This means, we can use the following straightforward mapping function \texttt{entity\_of}:
%
%\begin{verbatim}
%entity_of Endpoint          = {}
%entity_of Notification     = {}
%entity_of (TCB slots)       = Union (caps_of ` range slots)
%entity_of (CNode slots _)   = Union (caps_of ` range slots)
%entity_of (Untyped _ _)     = {}
%entity_of (ASIDPool slots)  = Union (caps_of ` range slots)
%entity_of (PT slots)        = Union (caps_of ` range slots)
%entity_of (PD slots)        = Union (caps_of ` range slots)
%entity_of (Frame _)         = {}
%entity_of (IOPT slots _)    = Union (caps_of ` range slots)
%entity_of (IODevice slots)  = Union (caps_of ` range slots)
%\end{verbatim}
%
%In this definition, \texttt{range slots} stands for the set of all capabilities in the range of the map \texttt{slots}. The function \texttt{Union} takes the union over a set of sets. The notation \texttt{f`A} stands for applying the function \texttt{f} to a set \texttt{A}. The function \texttt{caps\_of} translates capDL caps into sets of security model caps and is defined as follows. We abbreviate the entity notation as pairs \texttt{(entity\_id, rights)}.
%
%\begin{verbatim}
%caps_of NullCap = {}
%caps_of (EndpointCap id _ R) = {(id_of id, cap_rights R )}
%caps_of (NotificationCap id _ R) = {(id_of id, cap_rights R)}
%caps_of (UntypedCap id) = {(id_of id, {Create})}
%caps_of (CNodeCap id _ _ _ R) = {(id_of id, cnode_rights R)}
%caps_of (TCBCap id R) = {(id_of id, cap_rights R)}
%caps_of IRQControlCap =  {(id, {Read,Write,Grant}) | isIODevice id }
%caps_of (IRQHandlerCap id) =  {(id, {Read,Write,Grant})}
%caps_of (FrameCap id R) = {(id_of id, cap_rights R )}
%caps_of (PTCap id) = {(id_of id, {Read,Write})} 
%caps_of (PDCap id) = {(id_of id, {Read,Write})}
%caps_of ASIDControlCap = {(id, )}
%caps_of (ASIDPoolCap id)
%
%         | ASIDPoolCap { capObj :: ObjID }
%         | IOPortsCap { capObjs :: Set ObjID }
%         | IOSpaceMasterCap 
%         | IOSpaceCap { capObj :: ObjID }
%         | IOPTCap { capObj :: ObjID }
%\end{verbatim}
%
%cnode_rights = Read -> Take, Write -> Grant
%isIODevice id = true if objID id maps to an IODevice in the model
%
%
%This defines the mapping from capDL into the security model.

\end{document}
